Nuprl Lemma : msg-spec-loc-decl-implies 11,40

i:Id, ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), snd:msg-spec(dsda).
msg-spec-loc-decl(sndida msg-spec-loc(sndi
latex


DefinitionsIdLnk, t  T, x:AB(x), msg-spec-links(snd), (x  l), source(l), <ab>, Id, s = t, P  Q, x:AB(x), msg-spec-loc(sndi), msg-spec-loc-decl(sndida), Type, xt(x), fpf(Aa.B(a)), Knd, msg-spec(dsda), top, t.2, x.A(x), fpf-domain(f), x:A  B(x), t.1, msg-item(dsdakl), type List, atom{$n:n}, x:AB(x), b, P  Q, P  Q, guard(T), sq_type(T), prop{i:l}, sqequal(st), idlnk-deq, Kind-deq, product-deq(ABab), P  Q, left + right
Lemmasmember-fpf-domain, product-deq wf, Kind-deq wf, idlnk-deq wf, IdLnk sq, fpf-trivial-subtype-top, msg-item wf, pi1 wf, top wf, member map, fpf-domain wf, pi2 wf, msg-spec-loc-decl wf, msg-spec wf, Knd wf, fpf wf, Id wf, l member wf, msg-spec-links wf, IdLnk wf

origin